$\forall$${\it es}$:ES, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type. @$i$ discrete ${\it ds}$ $\Rightarrow$ (discrete state@$i$ $\subseteq$r State(${\it ds}$))